FDL - Nuprl Lemma : es-real-and

Nuprl Lemma : es-real-and_wf

11,40

P, Q:(ES{i}

{i'}), X:es-real{i:l}(es.P(es)), Y:es-real{i:l}(es.Q(es)),

p:R-compat{i:l}

p:R-compat((X.1); (Y.1)).
es-real-and{i:l}(P; Q; X; Y; p)

es-real{i:l}(es.(P(es) & Q(es)))

Definitions x. t(x), P Q, t.2, x:A. B(x), es-real-and{i:l}(P;Q;X;Y;p), P & Q, t T, t.1, x(s), es.P(es), , x:A. B(x)

Lemmas event system wf, es-real wf, Rplus wf, R-compat wf, R-realizes wf, es realizer wf

Definitions	x. t(x), P Q, t.2, x:A. B(x), es-real-and{i:l}(P;Q;X;Y;p), P & Q, t T, t.1, x(s), es.P(es), , x:A. B(x)
Lemmas	event system wf, es-real wf, Rplus wf, R-compat wf, R-realizes wf, es realizer wf